The present disclosure relates to formal verification in general, and to model checking of liveness properties in particular.
Computerized devices are an important part of the modern life. They control almost every aspect of our life—from writing documents to controlling traffic lights. However, computerized devices are bug-prone, and thus require a testing phase in which the bugs should be discovered. The testing phase is considered one of the most difficult tasks in developing a computerized device. Many developers of computerized devices invest a significant portion, such as 70%, of the development cycle to discover erroneous behaviors of the computerized device, also referred to as a target computerized system. The target computerized system may comprise hardware, software, firmware, a combination thereof and the like.
During the testing phase formal verification techniques may be applied to verify that a predetermined property is held. Formal verification may utilize a model checker to verify that the predetermined property, also referred to as a specification, is held. A model, also referred to as a design, represents a set of Boolean variables and functions for determining their values depending on environment inputs and on a portion of the set of Boolean variables. The Boolean variables are also referred to as registers. The model therefore represents all possible behaviors of the target computerized system over discrete time, also referred to as cycles. A gate in a model represents a portion of the model having a value, such as a variable, an outcome of a function based on values of one or more variables and the like.
The predetermined property may be a safety properties, in case it may be refuted using a finite counter-example. The predetermined property may be a liveness property in case it may only be refuted using an infinite counter-example. For example, a safety property may state that a “bad” event never happens, and be refuted by showing an exemplary finite trace in which the last state comprises the “bad” event occurring; whereas a liveness property may state that a “good” event eventually happens, for example, that “Process A eventually enters the critical section”. A refutation of such liveness property may be provided by showing an infinite trace in which the “good” event never occurs.
Some additional exemplary liveness properties may be “starvation freedom”, e.g., ensuring that the progress is always made; termination, e.g. ensuring that the final instruction may always be completed; “guaranteed service”, e.g. a service may always be eventually serviced and the like.
A counter-example for a liveness property is a description of an infinite behavior of the target computerized system. The infinite behavior is described using a finite number of states which are divided to a prefix and a suffix. The suffix also referred to as a loop or a repetitive portion of the counter-example, represents a repetitive behavior of a finite number of states for which the first state occurs after the last state, and therefore describe an infinite behavior.
In order to insure an “interesting” counter-example, the model may be required to comply with a fairness property. For example, in a model of a priority queue in which a message of high priority is passed before a message of low priority, a liveness property requiring that eventually every low priority message is removed from the queue may be refuted by a scenario in which in every cycle a new high priority message is received. An exemplary fairness property would require the input to provide both low priority and high priority messages.
In order to increase efficiency of the model checker, phase abstraction may be applied on an original model, producing a phase abstracted model. Phase abstraction is a technique that may reduce the size of a model by unfolding the transition relation function of the model, such that the transition relation function of the phase abstracted model represents more than one transitions in the model. Some may view a phase abstracted model as a model in which each cycle represents several cycles in the original model.